((VARTYPECTR? . 0) (CYCLE (NIL . (DECL (X Y Z X1 X2 X3 Y1 Y2 Y3 Z1 Z2 Z3) (OT& . GROUND) VARIABLE SEXP) . NIL . ((Z3 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Z3 .)) (Z1 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Z1 .)) (Y2 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Y2 .)) (X3 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . X3 .)) (X1 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . X1 .)) (Y . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Y .)) (SEXP . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . SEXP . PREFIX . 1000 .) . 1 . SEXP .)) (X . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . X .)) (Z . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Z .)) (X2 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . X2 .)) (Y1 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Y1 .)) (Y3 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Y3 .)) (Z2 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Z2 .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 1 .) (NIL . (DECL (A B C A1 A2 B1 B2 C1 C2) (OT& . GROUND) VARIABLE ATOM) . NIL . ((C2 . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . C2 .)) (B2 . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . B2 .)) (A2 . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . A2 .)) (C . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . C .)) (A . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . A .)) (ATOM . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . ATOM . PREFIX . 1000 .) . 2 . ATOM .)) (B . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . B .)) (A1 . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . A1 .)) (B1 . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . B1 .)) (C1 . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . C1 .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 2 .) (NIL . (DECL (TT NNIL) (OT& . GROUND) CONSTANT ATOM) . NIL . ((NNIL . (CONSTANT . GROUND . ATOM . NIL . NIL . 3 . NNIL .)) (ATOM . 2) (TT . (CONSTANT . GROUND . ATOM . NIL . NIL . 3 . TT .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 3 .) (NIL . (DECL (G G1 G2 G3) (OT& . GROUND) VARIABLE) . NIL . ((G3 . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 4 . G3 .)) (G1 . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 4 . G1 .)) (G . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 4 . G .)) (G2 . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 4 . G2 .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 4 .) (NIL . (DECL (CAR CDR) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((CDR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 5 . CDR .)) (CAR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 5 . CAR .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 5 .) (NIL . (DECL (CONS) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((CONS . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 6 . CONS .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 6 .) (NIL . (DECL (PHI) (OT& (GROUND) . TRUTHVAL) VARIABLE) . NIL . ((PHI . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 7 . PHI .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 7 .) ((((∀ G)) (⊃ (ATOM G) (SEXP G))) . (AXIOM (TM& ((∀ G)) (⊃ (ATOM G) (SEXP G)))) . NIL . ((SEXP . 1) (ATOM . 2) (G . 4)) . NIL . NIL . NIL . (8) . NIL . CYCLE . NIL . NIL . 8 .) ((((∀ X Y)) (SEXP (CONS X Y))) . (AXIOM (TM& ((∀ X Y)) (SEXP (CONS X Y)))) . NIL . ((X . 1) (SEXP . 1) (Y . 1) (CONS . 6)) . NIL . NIL . NIL . (9) . NIL . CYCLE . NIL . NIL . 9 .) ((((∀ G)) (⊃ (SEXP G) (∨ (ATOM G) (((∃ X Y)) (= G (CONS X Y)))))) . (AXIOM (TM& ((∀ G)) (⊃ (SEXP G) (∨ (ATOM G) (((∃ X Y)) (= G (CONS X Y))))))) . NIL . ((X . 1) (SEXP . 1) (Y . 1) (ATOM . 2) (G . 4) (CONS . 6)) . NIL . NIL . NIL . (10) . NIL . CYCLE . NIL . NIL . 10 .) ((((∀ X Y)) (¬ (ATOM (CONS X Y)))) . (AXIOM (TM& ((∀ X Y)) (¬ (ATOM (CONS X Y))))) . NIL . ((X . 1) (Y . 1) (ATOM . 2) (CONS . 6)) . NIL . NIL . NIL . (11) . NIL . CYCLE . NIL . NIL . 11 .) ((((∀ X Y)) (= (CAR (CONS X Y)) X)) . (AXIOM (TM& ((∀ X Y)) (= (CAR (CONS X Y)) X))) . NIL . ((X . 1) (Y . 1) (CAR . 5) (CONS . 6)) . NIL . NIL . NIL . (12) . NIL . CYCLE . NIL . NIL . 12 .) ((((∀ X Y)) (= (CDR (CONS X Y)) Y)) . (AXIOM (TM& ((∀ X Y)) (= (CDR (CONS X Y)) Y))) . NIL . ((X . 1) (Y . 1) (CDR . 5) (CONS . 6)) . NIL . NIL . NIL . (13) . NIL . CYCLE . NIL . NIL . 13 .) ((((∀ PHI A)) (∧ (PHI A) (((∀ X Y)) (⊃ (⊃ (∧ (PHI X) (PHI Y)) (PHI (CONS X Y))) (((∀ X)) (PHI X)))))) . (AXIOM (TM& ((∀ PHI)) (((∀ A)) (∧ (PHI A) (((∀ X Y)) (⊃ (⊃ (∧ (PHI X) (PHI Y)) (PHI (CONS X Y))) (((∀ X)) (PHI X)))))))) . NIL . ((X . 1) (Y . 1) (A . 2) (CONS . 6) (PHI . 7)) . NIL . NIL . NIL . (14) . NIL . CYCLE . NIL . NIL . 14 .) (NIL . (DECL (U V W U1 U2 U3 V1 V2 V3 W1 W2 W3) (OT& . GROUND) VARIABLE LIST) . NIL . ((W3 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . W3 .)) (W1 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . W1 .)) (V2 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . V2 .)) (U3 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . U3 .)) (U1 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . U1 .)) (V . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . V .)) (LIST . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . LIST . PREFIX . 1000 .) . 15 . LIST .)) (U . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . U .)) (W . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . W .)) (U2 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . U2 .)) (V1 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . V1 .)) (V3 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . V3 .)) (W2 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . W2 .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 15 .) (NIL . (DECL (NULL) (OT& (GROUND) . TRUTHVAL)) . NIL . ((NULL . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 16 . NULL .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 16 .) ((NULL NNIL) . (AXIOM (TM& NULL NNIL)) . NIL . ((NNIL . 3) (NULL . 16)) . NIL . NIL . NIL . (17) . NIL . CYCLE . NIL . NIL . 17 .) ((((∀ U)) (≡ (NULL U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (≡ (NULL U) (= U NNIL)))) . NIL . ((NNIL . 3) (U . 15) (NULL . 16)) . NIL . NIL . NIL . (18) . NIL . CYCLE . NIL . NIL . 18 .) ((LIST NNIL) . (AXIOM (TM& LIST NNIL)) . NIL . ((NNIL . 3) (LIST . 15)) . NIL . NIL . NIL . (19) . NIL . CYCLE . NIL . NIL . 19 .) ((((∀ G)) (⊃ (LIST G) (SEXP G))) . (AXIOM (TM& ((∀ G)) (⊃ (LIST G) (SEXP G)))) . NIL . ((SEXP . 1) (G . 4) (LIST . 15)) . NIL . NIL . NIL . (20) . NIL . CYCLE . NIL . NIL . 20 .) ((((∀ X U)) (¬ (NULL (CONS X U)))) . (AXIOM (TM& ((∀ X U)) (¬ (NULL (CONS X U))))) . NIL . ((X . 1) (CONS . 6) (U . 15) (NULL . 16)) . NIL . NIL . NIL . (21) . NIL . CYCLE . NIL . NIL . 21 .) (NIL . (DECL (*) (OT& (GROUND GROUND) . GROUND) CONSTANT UNIVERSAL INFIX 990) . NIL . ((* . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . (1 . * . INFIX . 990 .) . 22 . * .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 22 .) (NIL . (DECL (REVERSE) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((REVERSE . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 23 . REVERSE .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 23 .) (NIL . (DECL (RDC) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((RDC . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 24 . RDC .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 24 .) (NIL . (DECL (RAC) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((RAC . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 25 . RAC .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 25 .) (NIL . (DECL (SNOC) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((SNOC . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 26 . SNOC .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 26 .) ((((∀ X U)) (= (RDC X U) (CONDI (NULL U) NNIL (CONS X (RDC (CAR U) (CDR U)))))) . (AXIOM (TM& ((∀ X U)) (= (RDC X U) (CONDI (NULL U) NNIL (CONS X (RDC (CAR U) (CDR U))))))) . NIL . ((X . 1) (NNIL . 3) (CAR . 5) (CDR . 5) (CONS . 6) (U . 15) (NULL . 16) (RDC . 24)) . NIL . NIL . NIL . (27) . NIL . CYCLE . NIL . NIL . 27 .) ((((∀ X U)) (= (RAC X U) (CONDI (NULL U) X (RAC (CAR U) (CDR U))))) . (AXIOM (TM& ((∀ X U)) (= (RAC X U) (CONDI (NULL U) X (RAC (CAR U) (CDR U)))))) . NIL . ((X . 1) (CAR . 5) (CDR . 5) (U . 15) (NULL . 16) (RAC . 25)) . NIL . NIL . NIL . (28) . NIL . CYCLE . NIL . NIL . 28 .) ((((∀ X U)) (= (SNOC X U) (CONDI (NULL U) (CONS X NNIL) (CONS (CAR U) (SNOC X (CDR U)))))) . (AXIOM (TM& ((∀ X U)) (= (SNOC X U) (CONDI (NULL U) (CONS X NNIL) (CONS (CAR U) (SNOC X (CDR U))))))) . NIL . ((X . 1) (NNIL . 3) (CAR . 5) (CDR . 5) (CONS . 6) (U . 15) (NULL . 16) (SNOC . 26)) . NIL . NIL . NIL . (29) . NIL . CYCLE . NIL . NIL . 29 .) ((((∀ U V)) (= (REVERSE (* U V)) (* (REVERSE V) (REVERSE U)))) . (AXIOM (TM& ((∀ U V)) (= (REVERSE (* U V)) (* (REVERSE V) (REVERSE U))))) . NIL . ((U . 15) (V . 15) (* . 22) (REVERSE . 23)) . NIL . NIL . NIL . (30) . NIL . CYCLE . NIL . NIL . 30 .) ((((∀ X)) (= (REVERSE (CONS X NNIL)) (CONS X NNIL))) . (AXIOM (TM& ((∀ X)) (= (REVERSE (CONS X NNIL)) (CONS X NNIL)))) . NIL . ((X . 1) (NNIL . 3) (CONS . 6) (REVERSE . 23)) . NIL . NIL . NIL . (31) . NIL . CYCLE . NIL . NIL . 31 .) ((= (REVERSE NNIL) NNIL) . (AXIOM (TM& = (REVERSE NNIL) NNIL)) . NIL . ((NNIL . 3) (REVERSE . 23)) . NIL . NIL . NIL . (32) . NIL . CYCLE . NIL . NIL . 32 .) ((= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V)))) . (AXIOM (TM& = (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V))))) . NIL . ((CAR . 5) (CDR . 5) (CONS . 6) (U . 15) (V . 15) (NULL . 16) (* . 22)) . NIL . NIL . NIL . (33) . NIL . CYCLE . NIL . NIL . 33 .) (NIL . (DECL (H) (OT& (GROUND GROUND) . GROUND)) . NIL . ((H . (VARIABLE . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 34 . H .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 34 .) (NIL . (DECL (DREC) (OT& (GROUND ((GROUND GROUND) . GROUND)) (GROUND) . GROUND) CONSTANT) . NIL . ((DREC . (CONSTANT . ((GROUND ((GROUND GROUND) . GROUND)) (GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 35 . DREC .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 35 .) ((((∀ V H)) (⊃ (((∀ U V)) (⊃ (¬ (NULL U)) (LIST (H U V)))) (((∀ U)) (LIST ((DREC V H) U))))) . (AXIOM (TM& ((∀ V H)) (⊃ (((∀ U V)) (⊃ (¬ (NULL U)) (LIST (H U V)))) (((∀ U)) (LIST ((DREC V H) U)))))) . NIL . ((U . 15) (LIST . 15) (V . 15) (NULL . 16) (H . 34) (DREC . 35)) . NIL . NIL . NIL . (36) . NIL . CYCLE . NIL . NIL . 36 .) ((((∀ V H)) (⊃ (((∀ U V)) (⊃ (¬ (NULL U)) (LIST (H U V)))) (((∀ U)) (= ((DREC V H) U) (CONDI (NULL U) V (H U ((DREC V H) (CDR U)))))))) . (AXIOM (TM& ((∀ V H)) (⊃ (((∀ U V)) (⊃ (¬ (NULL U)) (LIST (H U V)))) (((∀ U)) (= ((DREC V H) U) (CONDI (NULL U) V (H U ((DREC V H) (CDR U))))))))) . NIL . ((CDR . 5) (U . 15) (LIST . 15) (V . 15) (NULL . 16) (H . 34) (DREC . 35)) . NIL . NIL . NIL . (37) . NIL . CYCLE . NIL . NIL . 37 .) (NIL . (DECL (APP) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((APP . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 38 . APP .))) . NIL . NIL . NIL . NIL . NIL . CYCLE . NIL . NIL . 38 .) ((((∀ U V)) (= (APP U V) ((DREC V (((λ U W)) (CONS (CAR U) W))) U))) . (AXIOM (TM& ((∀ U V)) (= (APP U V) ((DREC V (((λ U W)) (CONS (CAR U) W))) U)))) . NIL . ((CAR . 5) (CONS . 6) (W . 15) (U . 15) (V . 15) (DREC . 35) (APP . 38)) . NIL . NIL . NIL . (39) . NIL . CYCLE . NIL . NIL . 39 .) ((((∀ H)) (⊃ (((∀ U V)) (⊃ (¬ (NULL U)) (LIST (H U V)))) (((∀ U)) (LIST ((DREC V H) U))))) . (∀E V (TM& . V) (LN& . 36)) . NIL . ((U . 15) (LIST . 15) (V . 15) (NULL . 16) (H . 34) (DREC . 35)) . NIL . NIL . NIL . (36) . NIL . CYCLE . NIL . NIL . 40 .) ((⊃ (((∀ U V)) (⊃ (¬ (NULL U)) (LIST (CONS (CAR U) V)))) (((∀ U)) (LIST ((DREC V (((λ U W)) (CONS (CAR U) W))) U)))) . (∀E H (TM& ((λ U W)) (CONS (CAR U) W)) (LN& . 40)) . NIL . ((U . 15) (LIST . 15) (V . 15) (NULL . 16) (DREC . 35) (CAR . 5) (CONS . 6) (W . 15)) . NIL . NIL . NIL . (36) . NIL . CYCLE . NIL . NIL . 41 .) ((((∀ H)) (⊃ (((∀ U V)) (⊃ (¬ (NULL U)) (LIST (H U V)))) (((∀ U)) (= ((DREC V H) U) (CONDI (NULL U) V (H U ((DREC V H) (CDR U)))))))) . (∀E V (TM& . V) (LN& . 37)) . NIL . ((CDR . 5) (U . 15) (LIST . 15) (V . 15) (NULL . 16) (H . 34) (DREC . 35)) . NIL . NIL . NIL . (37) . NIL . CYCLE . NIL . NIL . 42 .) ((⊃ (((∀ U V)) (⊃ (¬ (NULL U)) (LIST (CONS (CAR U) V)))) (((∀ U)) (= ((DREC V (((λ U W)) (CONS (CAR U) W))) U) (CONDI (NULL U) V (CONS (CAR U) ((DREC V (((λ U W)) (CONS (CAR U) W))) (CDR U))))))) . (∀E H (TM& ((λ U W)) (CONS (CAR U) W)) (LN& . 42)) . NIL . ((CDR . 5) (U . 15) (LIST . 15) (V . 15) (NULL . 16) (DREC . 35) (CAR . 5) (CONS . 6) (W . 15)) . NIL . NIL . NIL . (37) . NIL . CYCLE . NIL . NIL . 43 .) ((⊃ (((∀ U V)) (⊃ (¬ (NULL U)) (LIST (CONS (CAR U) V)))) (((∀ U)) (= (APP U V) (CONDI (NULL U) V (CONS (CAR U) ((DREC V (((λ U W)) (CONS (CAR U) W))) (CDR U))))))) . (REWRITE LEFT (LN& . 43) (LR& 39)) . NIL . ((CDR . 5) (U . 15) (LIST . 15) (V . 15) (NULL . 16) (DREC . 35) (CAR . 5) (CONS . 6) (W . 15) (APP . 38)) . NIL . NIL . NIL . (37 39) . NIL . CYCLE . NIL . NIL . 44 .) ((= APP (((λ U V)) ((DREC V (((λ U W)) (CONS (CAR U) W))) U))) . (AXIOM (TM& = APP (((λ U V)) ((DREC V (((λ U W)) (CONS (CAR U) W))) U)))) . NIL . ((U . 15) (V . 15) (DREC . 35) (CAR . 5) (CONS . 6) (W . 15) (APP . 38)) . NIL . NIL . NIL . (45) . NIL . CYCLE . NIL . NIL . 45 .) ((⊃ (((∀ U V)) (⊃ (¬ (NULL U)) (LIST (CONS (CAR U) V)))) (((∀ U)) (= (APP U V) (CONDI (NULL U) V (CONS (CAR U) ((DREC V (((λ U W)) (CONS (CAR U) W))) (CDR U))))))) . (REWRITE LEFT (LN& . 44) (LR& 45)) . NIL . ((CDR . 5) (U . 15) (LIST . 15) (V . 15) (NULL . 16) (DREC . 35) (CAR . 5) (CONS . 6) (W . 15) (APP . 38)) . NIL . NIL . NIL . (37 39 45) . NIL . CYCLE . NIL . NIL . 46 .) ((⊃ (LIST (CDR U)) (((∀ V)) (= (APP (CDR U) V) ((DREC V (((λ U W)) (CONS (CAR U) W))) (CDR U))))) . (∀E U (TM& CDR U) (LN& . 39)) . NIL . ((CAR . 5) (CONS . 6) (W . 15) (U . 15) (V . 15) (DREC . 35) (APP . 38) (CDR . 5) (LIST . 15)) . NIL . NIL . NIL . (39) . NIL . CYCLE . NIL . NIL . 47 .) ((LIST (CDR U)) . (ASSUME (TM& LIST (CDR U))) . NIL . ((LIST . 15) (CDR . 5) (U . 15)) . NIL . NIL . NIL . (48) . NIL . CYCLE . NIL . NIL . 48 .) ((((∀ V)) (= (APP (CDR U) V) ((DREC V (((λ U W)) (CONS (CAR U) W))) (CDR U)))) . (⊃E (LN& . 47) (LN& . 48)) . NIL . ((CAR . 5) (CONS . 6) (W . 15) (U . 15) (V . 15) (DREC . 35) (APP . 38) (CDR . 5)) . NIL . NIL . NIL . (39 48) . NIL . CYCLE . NIL . NIL . 49 .) ((= (APP (CDR U) V) ((DREC V (((λ U W)) (CONS (CAR U) W))) (CDR U))) . (∀E V (TM& . V) (LN& . 49)) . NIL . ((CAR . 5) (CONS . 6) (W . 15) (U . 15) (V . 15) (DREC . 35) (APP . 38) (CDR . 5)) . NIL . NIL . NIL . (39 48) . NIL . CYCLE . NIL . NIL . 50 .) ((⊃ (LIST (CDR U)) (= (APP (CDR U) V) ((DREC V (((λ U W)) (CONS (CAR U) W))) (CDR U)))) . (⊃I (LN& . 48) (LN& . 50)) . NIL . ((LIST . 15) (CDR . 5) (U . 15) (CAR . 5) (CONS . 6) (W . 15) (V . 15) (DREC . 35) (APP . 38)) . NIL . NIL . NIL . (39) . NIL . CYCLE . NIL . NIL . 51 .) ((⊃ (((∀ U4 V4)) (⊃ (¬ (NULL U4)) (LIST (CONS (CAR U4) V4)))) (((∀ U5)) (= (APP U5 V) (CONDI (NULL U5) V (CONS (CAR U5) ((DREC V (((λ U6 W)) (CONS (CAR U6) W))) (CDR U5))))))) . (REWRITE LEFT (LN& . 46) (LR& 51)) . NIL . ((CDR . 5) (LIST . 15) (V . 15) (NULL . 16) (DREC . 35) (CAR . 5) (CONS . 6) (W . 15) (APP . 38) (U4 . (VARIABLE . GROUND . LIST . NIL . NIL . 52 . U4 .)) (V4 . (VARIABLE . GROUND . LIST . NIL . NIL . 52 . V4 .)) (U5 . (VARIABLE . GROUND . LIST . NIL . NIL . 52 . U5 .)) (U6 . (VARIABLE . GROUND . LIST . NIL . NIL . 52 . U6 .))) . NIL . NIL . NIL . (37 45 39) . NIL . CYCLE . NIL . NIL . 52 .)))